!pip  -q install --upgrade pyprover9
import pyprover9

ASSUMPTIONS = """

    % SORT AXIOMS: Establish two sorts.
    all x (Entity(x) | World(x)).
    all x -(Entity(x) & World(x)).
    all w all v (A(w,v) -> World(w) & World(v)).
    all a all w (In(a,w) -> Entity(a) & World(w)).
    World(aw).

    % W-PSR: for every entity, there exists, in some actual or non-actual world, a reason
    all a ( Entity(a) -> exists b exists u ( Entity(b) & World(u) & R(b,a) & In(b,u) ) ).
    
"""

GOAL = """
    % WL-PSR*: in w,for every actual contingent entity, there exists, in some actual or non-actual world, a reason
    all a ( Entity(a) & World(aw) & In(a, aw) & (exists v (World(v) & -In(a,v))) -> exists b exists u ( Entity(b) & World(u) & R(b,a) & In(b,u) ) ).

% If "Proved", then: WL-PSR* is weaker than L-PSR

"""

pyprover9.prove( ASSUMPTIONS, GOAL)